COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	COMMENT$ Here is a set of first order axioms for the integers based on
C00005 ENDMK
C⊗;
COMMENT$ Here is a set of first order axioms for the integers based on
the successor operation written SUCC and the predecessor operation
written PRED.  While the axioms don't mention sets, they are compatible
with a later imbedding into set theory, because the SORT mechanism of
FOL relativizes the axioms to the domain NATNUM, so other domains are
possible.  These axioms contain more than is logically necessary in
order to make proofs easier.$


DECLARE INDVAR I I1 I2 I3 J J1 J2 J3
K K1 K2 K3 L L1 L2 L3
M M1 M2 M3 N N1 N2 N3
 ε NATNUM;
DECLARE OPCONST SUCC: NATNUM → NATNUM [PRE];
DECLARE OPCONST PRED: NATNUM → INTEGER [PRE];
DECLARE INDVAR X Y Z;
DECLARE PREDPAR P(NATNUM);


AXIOM PRED:	∀N.(¬N=0 ⊃ NATNUM(PRED N));;

AXIOM PEANO:	∀N.(¬SUCC N = 0),
		∀N.PRED SUCC N = N,
		∀N.(¬N=0 ⊃ SUCC PRED N = N);;

AXIOM ONE:	SUCC 0 = 1;;

AXIOM INDUCTION:P(0) ∧ ∀N.(P(N) ⊃ P(SUCC N)) ⊃ ∀N.P(N);;


COMMENT$ The rest of these axioms are really just definitions.$

DECLARE OPCONST +(NATNUM,NATNUM)=NATNUM[R←475,L←470];
DECLARE PREDCONST ≥(NATNUM,NATNUM)[INF];
DECLARE PREDCONST >(NATNUM,NATNUM)[INF];
DECLARE OPCONST *(NATNUM,NATNUM)=NATNUM[R←555,L←550];
DECLARE OPCONST -(NATNUM,NATNUM)=INTEGER[R←455,L←450];

AXIOM PLUS:	∀M.(M+0=M),
		∀M N.(M+SUCC N =SUCC(M+N)),
		∀M N.(M+N=N+M)
		∀M N K.M+(N+K)=(M+N)+K
;;

AXIOM TIMES:	∀M. M*0=0,
		∀M.M*1=M,
		∀M N. M*SUCC N = M*N+M,
		∀M N. M*N=N*M,
		∀M N K. M*(N*K)=(M*N)*K
;;

AXIOM DISTRIB:	∀M N K.M*(N+K)=M*N+M*K;;


AXIOM MINUS:	∀M N. (M ≥ N ⊃ NATNUM(M-N)),
		∀M. M-0 = M,
		∀M N. (M - SUCC N = PRED(M - N)),
		∀N.N-N=0,
		∀M N K.(M+N)-K=M+(N-K);;


AXIOM GREATER:	∀M. M≥0,
		∀M. (0≥M ⊃ M=0),
		∀M N. (¬M=0 ∧ ¬N=0 ∧ M≥N ≡ PRED M ≥ PRED N),
		∀M N.(M>N ≡ M≥N ∧ ¬(M=N)),
		∀M N.(M≥N ≡ ∃K.(M=N+K)),
		∀M N K. (M>N ∧ N≥K ⊃ M>K),
		∀M N K. (M≥N ∧ N>K ⊃ M>K),
		∀M N K. (M≥N ∧ N≥K ⊃ M≥K);;